import Mathlib.Data.Real.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Real

-- 先给 Mathlib 写翻译
/--
**全集**（`Set.univ`）是类型 `α` 上包含 `α` 所有元素的集合。

  在概念上，它与类型 `α` 本身是“相同的”（在集合论中，它们实际上是同一个对象）。但在类型理论中，我们区分 `α` 是一个类型，而 `Set.univ` 是类型 `Set α` 的一个项（即集合）。此外，`Set.univ` 本身可以被强制转换为一个类型 `↥Set.univ`，该类型与 `α` 存在一一对应关系（双射），但两者在形式上是不同的。-/
abbrev «全集» {α : Type*} := Set.univ (α := α)

/-- 关系 `r` 两两成立的条件是 `r i j` 对任意 `i ≠ j` 都成立. -/
abbrev «两两» (r : α → α → Prop) := Pairwise (r := r)

/-- 格中的两个元素，如果它们的下确界是底元素，我们就说它们不交。
（这推广了集合不交的概念，后者可视为子集格中的成员。）

请注意，我们在此定义中并未引用运算符 `⊓`，因为这样可以在下确界不唯一、或者实现 `Inf` 需要额外的 `Decidable` 参数的序结构中讨论这一概念。 -/
abbrev «不交» [PartialOrder α] [OrderBot α] (a b : α) := Disjoint (a := a) (b := b)

-- 翻译到此结束

-- 样本空间 Ω 就是一个类型
variable {Ω : Type*}


/-- σ-代数（Sigma-Algebra）的定义：

设 Ω 是样本空间，F 是 Ω 的一些子集组成的集合，如果 F 满足以下条件：
1. 空集 ∅ 属于 F
2. 若 A 属于 F，则其补集 Ω \ A 也属于 F
3. 若 A₁, A₂, A₃, ... 是 F 中的可列个集合，则它们的并集 ⋃ₙ Aₙ 也属于 F

那么 F 称为 Ω 上的一个 σ-代数。-/
class «σ代数»  (Ω : Type*) (F : Set (Set Ω)) : Prop where
  -- 条件1：空集属于 F
  «有空集» : ∅ ∈ F
  -- 条件2：补集封闭
  «补集封闭» : ∀ A ∈ F, Aᶜ ∈ F
  -- 条件3：可列并封闭
  «可列并封闭» : ∀ (A : ℕ → Set Ω), (∀ n, A n ∈ F) → (⋃ n, A n) ∈ F

abbrev «事件域» := «σ代数»

-- 样本空间的所有子集构成的集合是样本空间上的一个σ代数
example : «σ代数» Ω «全集» :=
{
  «有空集» := by trivial
  «补集封闭» := fun A _ => by trivial
  «可列并封闭» := fun A _ => by trivial
}

/-! ## 可测空间

可测空间是由样本空间和其上的σ-代数组成的对，为定义概率测度提供基础。
-/
-- 可测空间（Measurable Space）的定义：由样本空间 Ω 和其上的一个 σ-代数 F 组成的对 -/


/-! ## 概率测度

概率测度是定义在σ-代数上的函数，满足非负性、规范性和可列可加性。
-/

/-- 概率测度的公理化定义（Kolmogorov 公理）

设 (Ω, F) 是一个可测空间，P : F → ℝ 是一个函数，如果 P 满足以下三条公理：

1. 非负性：对于任意事件 A ∈ F，有 P(A) ≥ 0
2. 规范性：P(Ω) = 1
3. 可列可加性（σ-可加性）：对于任意一列两两互不相交的事件 A₁, A₂, ... ∈ F，
   有 P(⋃ₙ Aₙ) = ∑ₙ P(Aₙ)

则称 P 为定义在 (Ω, F) 上的概率测度 -/
class «概率» {Ω : Type*} (F : Set (Set Ω)) [«σ代数» Ω F]
  (P : (Set Ω) → ℝ) : Prop where
  -- 公理1：非负性
  «非负» : ∀ A : Set Ω, A ∈ F → 0 ≤ P A

  -- 公理2：规范性
  «正规» : P («全集» : Set Ω) = 1

  -- 公理3：可列可加性
  «可列可加» : ∀ (A : ℕ → Set Ω),
    (∀ n, A n ∈ F) →
    («两两» fun i j => «不交» (A i) (A j)) →
    P (⋃ n, A n) = ∑' n, P (A n)

/-- 空集的概率为零。 -/
theorem «空集概率为零» {Ω : Type*} (F : Set (Set Ω)) {h1: «σ代数» Ω F}
  (P : (Set Ω) → ℝ) {h2: «概率» F P} :
  P ∅ = 0 := by
  -- 利用 ∅ ⊔ ∅ = ∅ 和 ∅ ⊓ ∅ = ∅ 的性质
  -- 考虑可列并 ⋃ₙ ∅ = ∅
  let A : ℕ → Set Ω := fun _ => ∅
  -- 验证 A n ∈ F 对所有 n 成立
  have «A n 属于 F» : ∀ n, A n ∈ F := fun _ => «σ代数».«有空集»
  -- 验证 A 是两两不交的
  have «A n 两两不交» : «两两» fun i j => «不交» (A i) (A j) := by
    intro i j hij
    aesop
  -- 应用可列可加性
  have «应用可列可加» : P (⋃ n, A n) = ∑' n, P (A n) := «概率».«可列可加»  A «A n 属于 F» «A n 两两不交»
  -- 计算并集
  have «全体 A n 的并集是空集» : (⋃ n, A n) = ∅ := by
    ext x
    simp [A]
  -- 代入
  rw [«全体 A n 的并集是空集»] at «应用可列可加»
  unfold A at «应用可列可加»
  -- 得到 P(∅) = ∑' n, P(∅)
  -- 如果 P(∅) > 0，则右边发散，与左边是实数矛盾
  -- 因此必须 P(∅) = 0
  have «应用非负性» : 0 ≤ P ∅ := «概率».«非负» ∅ h1.«有空集»
  by_cases h : P ∅ = 0
  · exact h
  · have «概率恒正» : 0 < P ∅ := lt_of_le_of_ne «应用非负性» (Ne.symm h)
    have «级数发散» : ¬Summable fun (n : ℕ) => P ∅ := by aesop
    aesop
#min_imports
